A, B:Type, xs, ys:A List. strong-subtype(A;B)  {xs  ys  xs  ys} 

latex

Definitions	A & B, strong-subtype(A;B), t  T, x:A. B(x), S  T, l1  l2, P  Q, {T}, x:A. B(x), (x  l), P  Q, P  Q, P & Q, P  Q, as @ bs, Prop
Lemmas	strong-subtype-eq3, strong-subtype-list, append wf, strong-subtype-l member-type, member append, list-subtype, subtype rel list, l member wf, iseg wf, strong-subtype wf